T:Type, X:MaInterface(T), es:ES, e:E.
(ma-in-interface(es;X;e))  (loc(e)  ma-interface-locs(X)) 

latex

Definitions

False, t  T, P  Q, Id, f(x), t.2, Knd, Top, a:A fp B(a), b, (x  l), x:A. B(x), kind(e), KindDeq, , MaInterface(T), x:AB(x), A, b, s = t, , x:A  B(x), P & Q, P  Q, Unit, left + right, ma-in-interface(es;X;e), E, ES, Type, loc(e), IdDeq, x  dom(f), {x:A| B(x)} , State(ds), hasloc(k;i), x. t(x), x.A(x), t.1, ma-interface-locs(I), if b then t else f fi , type List, Void, x:A.B(x), let x,y = A in B(x;y), case b of inl(x) => s(x) | inr(y) => t(y), <a, b>, S  T, IdLnk

Lemmas

subtype rel product, subtype rel list, IdLnk wf, subtype rel function, subtype rel set, l member wf, subtype-set-hasloc, member-fpf-domain, pi2 wf, fpf-trivial-subtype-top, fpf wf, hasloc wf, decl-state wf, top wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, Id wf, id-deq wf, es-loc wf, bool wf, assert wf, fpf-dom wf, Knd wf, Kind-deq wf, es-kind wf, false wf